Step of Proof: fun_with_inv_is_bij 12,41
Inference at * 1 1 2 1 
Iof proof for Lemma fun with inv is bij:



1. A : Type
2. B : Type
3. f : AB
4. g : BA
5. (g o f) = Id{A}
6. (f o g) = Id{B}
7. b : B
  f(g(b)) = b 
latex
 by ((With b (EqHD 6)) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 
latex

C1: 

C1: 6. b : B
C1: 7. (f o g)(b) = Id{B}(b)
C1:   f(g(b)) = b
C.

origin